1. Field of the Invention
The present invention relates to a logical equivalence verifying device, a logical equivalence verifying method and a logical equivalence verifying program in which after logical equivalence between a pre-change one and a post-change one of a circuit being designed is verified when the circuit has been changed or altered, only those portions in which there is a difference or mismatch between the logic of the pre-change circuit and the logic of the post-change circuit are displayed, and in addition, when a large number of locations where logical mismatches are detected, the causes of common mismatches, which are elements of the causes of common logical mismatches between the pre-change circuit and the post-change circuit, are analyzed.
2. Description of the Related Art
A logical equivalence verifying technology for verifying logic designs of large-scale integrated (LSI) circuits or the like is one of computer-aided design (CAD) technologies, and the development of LSI circuits includes a multitude of processes, starting from specification study until final LSI manufacture. As a result, it is very important that errors or mistakes in logic designs should not come in during a design process in order to develop LSI circuits of high quality.
After a logic specification has been fixed in the design process, changes in the actual configuration of a logic circuit, such as insertion of a scan circuit for signal timing adjustments, manufacturing tests, etc., are frequently carried out in implementation design processes for actual manufacture without altering the logic specification. Such work is called an implementation process, in which there is a high possibility of errors or mistakes being introduced therein to change the logic. Therefore, it is necessary to improve the quality of the logic design by verifying whether the logic specifications of the logic circuits before and after the implementation match or coincide with each other. The technology for this purpose is a logical equivalence verification technology. Hereinafter, the logic circuit before the implementation process is called “specification”, and the logic circuit after the implementation process is called “implementation”.
First of all, a plurality of verification points are selected in the logic circuit before logical equivalence verification is performed. For the verification points, those points at which the circuit can be easily cut, such as external terminals, flip-flops (FF) or the like of an LSI circuit, are usually selected. Then, a portion of the circuit having a certain verification point as an output point is extracted as a logic cone. Here, note that the logic cone is a portion of the circuit backtraced or backtracked from the verification point extracted as the output point to other verification points which become input points.
FIG. 23 is a view showing one example of such a logic cone. As shown in FIG. 23, a logic cone 51 is a portion backtraced from a verification point 52, which serves as an output point, to verification points 53, 54, which serve as input points. In addition, the verification points 53, 54 are also output points of other logic cones. Though each logic cone is usually not so large, several thousand to several ten or hundred thousand logic cones are cut out from a single LSI circuit, so that logical equivalence verification for each logic cone is performed. When the logics of all the logic cones become matched or in coincidence, the two logic circuits, i.e., an implementation and a specification, are finally considered to be equivalent to each other, whereas when they become mismatched or out of coincidence, the logics of a plurality of logic cones often become mismatched, so analysis also becomes difficult. For instance, when the logic cone 51 and the logic cone 55 overlap with each other, as shown in FIG. 23, it is verified that both the logic cones 51, 55 do not match each other if design errors or mistakes are induced into the overlapping portions thereof.
Though the logic of the specification and the logic of the implementation are expected to coincide with each other, if the verification results become mismatched due to correction mistakes or the like, it is necessary to analyze its causes and correct the logic in an appropriate manner.
Also, for a logical equivalence verifying device which performs logical equivalence verification between a pre-change circuit and a post-change circuit and displays the results thereof, there is known one which displays non-coincident or mismatched portions when there exists a difference or mismatch between the logic of the pre-change circuit and the logic of the post-change circuit (for example, see a first patent document: Japanese Patent Application Laid-Open No 10-254923, pages 3, 4 and FIG. 1).
However, there arises a problem that the number of logic cones constituting one LSI circuit is huge, as mentioned above, so it requires a lot of time and trouble to specify the cause of mismatches after the logical equivalence verification. Moreover, the user selects sets of corresponding portions of the specification and the implementations in a plurality of logic cones which become mismatched after the logical equivalence verification, and examines differences between the specification and the implementation on their circuit diagrams so as to find the causes of mismatches, but he or she does not know that it is efficient from which of the mismatch causes the examination is started, thus resulting in quite a lot of number of investigations for the causes of mismatches.